$\forall$$T$:Type. subtype\_rel($T$; $\mathbb{Z}$) $\Rightarrow$ ($\forall$$x$:$T$, $L$:($T$ List). s{-}insert($x$; $L$) $\in$ ($T$ List))